step(bs,al,tm(s,[ctxm(zeta_,sp,ip,ip_bs,ip_bs),ctxm(zeta_,u,ip,ip_al_3,ip_al_3)],pri(lst,[ctxm(zeta_,u,i_sess,ss(zeta_,i_sess),ss(zeta_,i_sess)),pri(enc,[ctxm(zeta_,dot,q,ss(zeta_,i_q),ss(zeta_,c_q)),pri(aka,[ctxm(zeta_,dot,kM_c,kM_c,kM_c),ctxm(zeta_,dot,n_a,ss(zeta_,i_n_a),ss(zeta_,c_n_a)),ctxm(zeta_,sp,kM,kM_bs,kM_bs),ctxm(zeta_,dot,n_b,ss(zeta_,i_n_b),ss(zeta_,c_n_b))])])]))).
